#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 110
for i in range(0,maxPrio):
  rank.append([])

# SOURCES AND REUSE LEMMAS

if lemma == "sqn_ue_invariance" or \
     lemma == "sqn_hss_invariance" or \
     lemma == "sqn_ue_src" or \
     lemma == "sqn_hss_src":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*Sqn_UE\(.*', line): rank[90].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[90].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[95].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[95].append(num)

elif lemma == "sqn_ue_nodecrease":
  for line in lines:
    num = line.split(':')[0]    
    if re.match('.*\(last\(#j.*', line): rank[100].append(num)
    elif re.match('.*Sqn_UE_Change\(.*', line): rank[90].append(num)
    elif re.match('.*\(#vr < #i\).*', line): rank[80].append(num)
    elif re.match('.*Sqn_UE\(.*count.1.*', line): rank[70].append(num)

# AGREEMENTS LEMMAS

elif   lemma == "injectiveagreement_ue_hss_kseaf_noKeyRev" or \
       lemma == "noninjectiveagreement_ue_hss_snname_noKeyRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[95].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[90].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[80].append(num)
    elif re.match('.*!HSS\(.*', line): rank[70].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[65].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[65].append(num)
    elif re.match('.*St_4_SEAF\(.*', line): rank[65].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[65].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[65].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[60].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[50].append(num)
    elif re.match('.*Commit\(.*', line): rank[40].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[30].append(num)
    elif re.match('.*RcvS\(.*<\'aia\'.*', line): rank[10].append(num)

# EXECUTABILITY LEMMAS

elif lemma == "executability_honest":
  for line in lines:
    num = line.split(':')[0]  
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[99].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[99].append(num)
    elif re.match('.*RcvS\(.*', line): rank[98].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[90].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[87].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[86].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[85].append(num)
    elif re.match('.*!KU\( f5\(~k.*', line): rank[84].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[83].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[72].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[60].append(num)
    elif re.match('.*!KD\( \(f5\(.*', line): rank[60].append(num)


elif lemma == "executability_resync" or \
     lemma == "executability_desync":
  for line in lines:
    num = line.split(':')[0]  
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!HSS\(.*', line): rank[99].append(num)
    elif re.match('.*=.*=.*', line): rank[98].append(num)
    elif re.match('.*<.*=.*', line): rank[97].append(num)
    elif re.match('.*HSS_Resync_End\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line): rank[95].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[95].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[94].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[94].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[94].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[94].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[93].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[93].append(num)
    elif re.match('.*~~>.*', line): rank[92].append(num)
    elif re.match('.*!Ltk_Sym\(.*', line): rank[90].append(num)
    elif re.match('.*RcvS\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[60].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f1_star\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[30].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[20].append(num)
    elif re.match('.*!KD\( \(f5\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( \(f5_star\(.*', line): rank[20].append(num)
    elif re.match('.*!KD\( \(f5_star\(.*', line): rank[20].append(num)


else:
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    sys.stderr.write(goal)
    print goal

